(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const _1-0 (_ BitVec 1))
(declare-const v17 Bool)
(declare-const v19 Bool)
(declare-const _21-0 (_ BitVec 21))
(assert (or (bvuge _1-0 _1-0) (= (= v0 v5 v6 v0 v2 v14 v15 v11 v6 v4) v19 v17 (and (bvuge _1-0 _1-0) v3 v2 v12 v6 v15 v5 v9 v15) v10 v17 v1 (bvuge _1-0 _1-0) v1) (= (= v0 v5 v6 v0 v2 v14 v15 v11 v6 v4) v19 v17 (and (bvuge _1-0 _1-0) v3 v2 v12 v6 v15 v5 v9 v15) v10 v17 v1 (bvuge _1-0 _1-0) v1)))
(check-sat)
